p:(IdLnk List), i:{0..||p||}, j:{0..(i+1)}.
lpath(p)  lconnects(l_interval(p;j;i);source(p[j]);source(p[i])) 

latex

Definitions	IdLnk, t  T, x:A. B(x), ||as||, {i..j}, lpath(p), lconnects(p;i;j), P  Q, False, A, P & Q, A  B, i  j < k, , True, l[i], lnk-inv(l), destination(l), Id, T, source(l), P  Q, P  Q, l_interval(l;j;i), {T}, SQType(T)
Lemmas	last l interval, hd l interval, l interval wf, length l interval, select l interval, le wf, squash wf, true wf, lsrc wf, not wf, Id wf, ldst wf, lnk-inv wf, select wf, lpath wf, int seg wf, length wf1, IdLnk wf